$\forall$$T$:Type, $b$:$\mathbb{B}$, $x$, $y$:$T$. ($\uparrow$$b$) $\Rightarrow$ (if $b$ then $x$ else $y$ fi  = $x$)